Search results for "guarded fragment"

showing 3 items of 3 documents

Finite Satisfiability of the Two-Variable Guarded Fragment with Transitive Guards and Related Variants

2018

We consider extensions of the two-variable guarded fragment, GF2, where distinguished binary predicates that occur only in guards are required to be interpreted in a special way (as transitive relations, equivalence relations, pre-orders or partial orders). We prove that the only fragment that retains the finite (exponential) model property is GF2 with equivalence guards without equality. For remaining fragments we show that the size of a minimal finite model is at most doubly exponential. To obtain the result we invent a strategy of building finite models that are formed from a number of multidimensional grids placed over a cylindrical surface. The construction yields a 2NExpTime-upper bou…

FOS: Computer and information sciencesComputer Science - Logic in Computer ScienceTwo-variable logicGeneral Computer ScienceComputational complexity theoryLogicguarded fragmentBinary number0102 computer and information sciences01 natural sciencesUpper and lower boundsTheoretical Computer ScienceCombinatoricstransitive relationEquivalence relationfinite satisfiability problem0101 mathematicsEquivalence (formal languages)Integer programmingMathematicsDiscrete mathematicsTransitive relationNEXPTIMEcomputational complexity010102 general mathematicsLogic in Computer Science (cs.LO)Computational Mathematics010201 computation theory & mathematicsequivalence ralationACM Transactions on Computational Logic
researchProduct

Adding Path-Functional Dependencies to the Guarded Two-Variable Fragment with Counting

2017

The satisfiability and finite satisfiability problems for the two-variable guarded fragment of first-order logic with counting quantifiers, a database, and path-functional dependencies are both ExpTime-complete.

FOS: Computer and information sciencesComputer Science - Logic in Computer ScienceTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESintegrity constraintssatisfiabilitycounting quantifierspath-functional dependenciesComputer Science::Logic in Computer Scienceguarded fragmentkey constraintstwo-variable fragmetLogic in Computer Science (cs.LO)
researchProduct

Equivalence closure in the two-variable guarded fragment

2015

We consider the satisfiability and finite satisfiability problems for the extension of the two-variable guarded fragment in which an equivalence closure operator can be applied to two distinguished binary predicates. We show that the satisfiability and finite satisfiability problems for this logic are 2-ExpTime-complete. This contrasts with an earlier result that the corresponding problems for the full two-variable logic with equivalence closures of two binary predicates are 2-NExpTime-complete.

Computational complexity theoryLogiccomputational complexityguarded fragmentsatisfiability problemBinary numberTheoretical Computer ScienceCombinatoricsArts and Humanities (miscellaneous)Computer Science::Logic in Computer ScienceClosure operatorEquivalence (formal languages)MathematicsDiscrete mathematicssatisfiability problemcomputational complexitydecidabilityequivalence closureSatisfiabilityDecidabilityTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESClosure (computer programming)Hardware and ArchitectureTheoryofComputation_LOGICSANDMEANINGSOFPROGRAMSBoolean satisfiability problemSoftwareJournal of Logic and Computation
researchProduct